
; Copyright (c) 2015 Microsoft Corporation
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(declare-const r1 Real)
(declare-const r2 Real)
(set-option :pp.flat-assoc false)
(set-option :pp.max-depth 1000)


(simplify (* (/ 1.0 2.0) 3.0))
(simplify (* (/ 3.0 2.0) 2.0))
(simplify (* (+ (* 3.0 r1) r2) (/ 1.0 2.0)))
(simplify (div 3 2))
(simplify (div 5 2))
(simplify (div (- 5) 2))
(simplify (mod 3 2))
(simplify (mod (+ a b) 1))
(simplify (mod (+ a b) 2))
(simplify (mod (+ a b 3) 2))
(simplify (mod (* a b 6) 2))
(simplify (mod (* a b 7) 5))
(simplify (rem 3 2))
(declare-fun f (Int) Int)       
(simplify (+ (f 1) (+ (f 2) (+ (f 3) (+ (f 4) (+ (f 5) (+ (f 6) (+ (f 7) (+ (f 8) (f 9)))))))))
                 :flat false)
(simplify (mod (+ (f 1) (+ (f 2) (+ (f 3) (+ (f 4) (+ (f 5) (+ (f 6) (+ (f 7) (+ (f 8) (f 9)))))))))
                      3)
                 :flat false)
(simplify (rem (+ (f 1) (+ (f 2) (+ (f 3) (+ (f 4) (+ (f 5) (+ (f 6) (+ (f 7) (+ (f 8) (f 9)))))))))
                      3)
                 :flat false)
(simplify (rem a 2))
(simplify (rem a (- 2)))
(simplify (rem a b))

(set-option :pp.flat-assoc true) ;; speedup pretty printing
(simplify (rem (+ (f 1) (+ (f 2) (+ (f 3) (+ (f 4) (+ (f 5) (+ (f 6) (+ (f 7) (+ (f 8) (+ (f 9) (+ (f 10)
                      (+ (f 11) (+ (f 12) (+ (f 13) (+ (f 14) (+ (f 15) (+ (f 16) (+ (f 17) (+ (f 18) (+ (f 19) (+ (f 20)
                      (+ (f 21) (+ (f 22) (+ (f 23) (+ (f 24) (+ (f 25) (+ (f 26) (+ (f 27) (+ (f 28) (+ (f 29) (+ (f 30)
                      (+ (f 31) (+ (f 32) (+ (f 33) (+ (f 34) (+ (f 35) (+ (f 36) (+ (f 37) (+ (f 38) (+ (f 39) (+ (f 40)
                      (+ (f 41) (+ (f 42) (+ (f 43) (+ (f 44) (+ (f 45) (+ (f 46) (+ (f 47) (+ (f 48) (+ (f 49) (+ (f 50)
                         (f 51)))))))))))))))))))))))))))))))))))))))))))))))))))
                      (- 3))
                 :flat false)
